1   /*                        __    __  __  __    __  ___
2    *                       \  \  /  /    \  \  /  /  __/
3    *                        \  \/  /  /\  \  \/  /  /
4    *                         \____/__/  \__\____/__/.ɪᴏ
5    * ᶜᵒᵖʸʳᶦᵍʰᵗ ᵇʸ ᵛᵃᵛʳ ⁻ ˡᶦᶜᵉⁿˢᵉᵈ ᵘⁿᵈᵉʳ ᵗʰᵉ ᵃᵖᵃᶜʰᵉ ˡᶦᶜᵉⁿˢᵉ ᵛᵉʳˢᶦᵒⁿ ᵗʷᵒ ᵈᵒᵗ ᶻᵉʳᵒ
6    */
7   package io.vavr.test;
8   
9   /*-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-*\
10     G E N E R A T O R   C R A F T E D
11  \*-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-*/
12  
13  import io.vavr.*;
14  import io.vavr.control.Option;
15  import io.vavr.control.Try;
16  import java.util.Objects;
17  import java.util.Random;
18  
19  /**
20   * A property builder which provides a fluent API to build checkable properties.
21   *
22   * @author Daniel Dietrich
23   */
24  public class Property {
25  
26      private final String name;
27  
28      private Property(String name) {
29          this.name = name;
30      }
31  
32      /**
33       * Defines a new Property.
34       *
35       * @param name property name
36       * @return a new {@code Property}
37       * @throws NullPointerException if name is null.
38       * @throws IllegalArgumentException if name is empty or consists of whitespace only
39       */
40      public static Property def(String name) {
41          Objects.requireNonNull(name, "name is null");
42          if (name.trim().isEmpty()) {
43              throw new IllegalArgumentException("name is empty");
44          }
45          return new Property(name);
46      }
47  
48      private static void logSatisfied(String name, int tries, long millis, boolean exhausted) {
49          if (exhausted) {
50              log(String.format("%s: Exhausted after %s tests in %s ms.", name, tries, millis));
51          } else {
52              log(String.format("%s: OK, passed %s tests in %s ms.", name, tries, millis));
53          }
54      }
55  
56      private static void logFalsified(String name, int currentTry, long millis) {
57          log(String.format("%s: Falsified after %s passed tests in %s ms.", name, currentTry - 1, millis));
58      }
59  
60      private static void logErroneous(String name, int currentTry, long millis, String errorMessage) {
61          log(String.format("%s: Errored after %s passed tests in %s ms with message: %s", name, Math.max(0, currentTry - 1), millis, errorMessage));
62      }
63  
64      private static void log(String msg) {
65          System.out.println(msg);
66      }
67  
68      /**
69       * Creates a CheckError caused by an exception when obtaining a generator.
70       *
71       * @param position The position of the argument within the argument list of the property, starting with 1.
72       * @param size     The size hint passed to the {@linkplain Arbitrary} which caused the error.
73       * @param cause    The error which occurred when the {@linkplain Arbitrary} tried to obtain the generator {@linkplain Gen}.
74       * @return a new CheckError instance.
75       */
76      private static CheckError arbitraryError(int position, int size, Throwable cause) {
77          return new CheckError(String.format("Arbitrary %s of size %s: %s", position, size, cause.getMessage()), cause);
78      }
79  
80      /**
81       * Creates a CheckError caused by an exception when generating a value.
82       *
83       * @param position The position of the argument within the argument list of the property, starting with 1.
84       * @param size     The size hint of the arbitrary which called the generator {@linkplain Gen} which caused the error.
85       * @param cause    The error which occurred when the {@linkplain Gen} tried to generate a random value.
86       * @return a new CheckError instance.
87       */
88      private static CheckError genError(int position, int size, Throwable cause) {
89          return new CheckError(String.format("Gen %s of size %s: %s", position, size, cause.getMessage()), cause);
90      }
91  
92      /**
93       * Creates a CheckError caused by an exception when testing a Predicate.
94       *
95       * @param cause The error which occurred when applying the {@linkplain java.util.function.Predicate}.
96       * @return a new CheckError instance.
97       */
98      private static CheckError predicateError(Throwable cause) {
99          return new CheckError("Applying predicate: " + cause.getMessage(), cause);
100     }
101 
102     /**
103      * Returns a logical for all quantor of 1 given variables.
104      *
105      * @param <T1> 1st variable type of this for all quantor
106      * @param a1 1st variable of this for all quantor
107      * @return a new {@code ForAll1} instance of 1 variables
108      */
109     public <T1> ForAll1<T1> forAll(Arbitrary<T1> a1) {
110         return new ForAll1<>(name, a1);
111     }
112 
113     /**
114      * Returns a logical for all quantor of 2 given variables.
115      *
116      * @param <T1> 1st variable type of this for all quantor
117      * @param <T2> 2nd variable type of this for all quantor
118      * @param a1 1st variable of this for all quantor
119      * @param a2 2nd variable of this for all quantor
120      * @return a new {@code ForAll2} instance of 2 variables
121      */
122     public <T1, T2> ForAll2<T1, T2> forAll(Arbitrary<T1> a1, Arbitrary<T2> a2) {
123         return new ForAll2<>(name, a1, a2);
124     }
125 
126     /**
127      * Returns a logical for all quantor of 3 given variables.
128      *
129      * @param <T1> 1st variable type of this for all quantor
130      * @param <T2> 2nd variable type of this for all quantor
131      * @param <T3> 3rd variable type of this for all quantor
132      * @param a1 1st variable of this for all quantor
133      * @param a2 2nd variable of this for all quantor
134      * @param a3 3rd variable of this for all quantor
135      * @return a new {@code ForAll3} instance of 3 variables
136      */
137     public <T1, T2, T3> ForAll3<T1, T2, T3> forAll(Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3) {
138         return new ForAll3<>(name, a1, a2, a3);
139     }
140 
141     /**
142      * Returns a logical for all quantor of 4 given variables.
143      *
144      * @param <T1> 1st variable type of this for all quantor
145      * @param <T2> 2nd variable type of this for all quantor
146      * @param <T3> 3rd variable type of this for all quantor
147      * @param <T4> 4th variable type of this for all quantor
148      * @param a1 1st variable of this for all quantor
149      * @param a2 2nd variable of this for all quantor
150      * @param a3 3rd variable of this for all quantor
151      * @param a4 4th variable of this for all quantor
152      * @return a new {@code ForAll4} instance of 4 variables
153      */
154     public <T1, T2, T3, T4> ForAll4<T1, T2, T3, T4> forAll(Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4) {
155         return new ForAll4<>(name, a1, a2, a3, a4);
156     }
157 
158     /**
159      * Returns a logical for all quantor of 5 given variables.
160      *
161      * @param <T1> 1st variable type of this for all quantor
162      * @param <T2> 2nd variable type of this for all quantor
163      * @param <T3> 3rd variable type of this for all quantor
164      * @param <T4> 4th variable type of this for all quantor
165      * @param <T5> 5th variable type of this for all quantor
166      * @param a1 1st variable of this for all quantor
167      * @param a2 2nd variable of this for all quantor
168      * @param a3 3rd variable of this for all quantor
169      * @param a4 4th variable of this for all quantor
170      * @param a5 5th variable of this for all quantor
171      * @return a new {@code ForAll5} instance of 5 variables
172      */
173     public <T1, T2, T3, T4, T5> ForAll5<T1, T2, T3, T4, T5> forAll(Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5) {
174         return new ForAll5<>(name, a1, a2, a3, a4, a5);
175     }
176 
177     /**
178      * Returns a logical for all quantor of 6 given variables.
179      *
180      * @param <T1> 1st variable type of this for all quantor
181      * @param <T2> 2nd variable type of this for all quantor
182      * @param <T3> 3rd variable type of this for all quantor
183      * @param <T4> 4th variable type of this for all quantor
184      * @param <T5> 5th variable type of this for all quantor
185      * @param <T6> 6th variable type of this for all quantor
186      * @param a1 1st variable of this for all quantor
187      * @param a2 2nd variable of this for all quantor
188      * @param a3 3rd variable of this for all quantor
189      * @param a4 4th variable of this for all quantor
190      * @param a5 5th variable of this for all quantor
191      * @param a6 6th variable of this for all quantor
192      * @return a new {@code ForAll6} instance of 6 variables
193      */
194     public <T1, T2, T3, T4, T5, T6> ForAll6<T1, T2, T3, T4, T5, T6> forAll(Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6) {
195         return new ForAll6<>(name, a1, a2, a3, a4, a5, a6);
196     }
197 
198     /**
199      * Returns a logical for all quantor of 7 given variables.
200      *
201      * @param <T1> 1st variable type of this for all quantor
202      * @param <T2> 2nd variable type of this for all quantor
203      * @param <T3> 3rd variable type of this for all quantor
204      * @param <T4> 4th variable type of this for all quantor
205      * @param <T5> 5th variable type of this for all quantor
206      * @param <T6> 6th variable type of this for all quantor
207      * @param <T7> 7th variable type of this for all quantor
208      * @param a1 1st variable of this for all quantor
209      * @param a2 2nd variable of this for all quantor
210      * @param a3 3rd variable of this for all quantor
211      * @param a4 4th variable of this for all quantor
212      * @param a5 5th variable of this for all quantor
213      * @param a6 6th variable of this for all quantor
214      * @param a7 7th variable of this for all quantor
215      * @return a new {@code ForAll7} instance of 7 variables
216      */
217     public <T1, T2, T3, T4, T5, T6, T7> ForAll7<T1, T2, T3, T4, T5, T6, T7> forAll(Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6, Arbitrary<T7> a7) {
218         return new ForAll7<>(name, a1, a2, a3, a4, a5, a6, a7);
219     }
220 
221     /**
222      * Returns a logical for all quantor of 8 given variables.
223      *
224      * @param <T1> 1st variable type of this for all quantor
225      * @param <T2> 2nd variable type of this for all quantor
226      * @param <T3> 3rd variable type of this for all quantor
227      * @param <T4> 4th variable type of this for all quantor
228      * @param <T5> 5th variable type of this for all quantor
229      * @param <T6> 6th variable type of this for all quantor
230      * @param <T7> 7th variable type of this for all quantor
231      * @param <T8> 8th variable type of this for all quantor
232      * @param a1 1st variable of this for all quantor
233      * @param a2 2nd variable of this for all quantor
234      * @param a3 3rd variable of this for all quantor
235      * @param a4 4th variable of this for all quantor
236      * @param a5 5th variable of this for all quantor
237      * @param a6 6th variable of this for all quantor
238      * @param a7 7th variable of this for all quantor
239      * @param a8 8th variable of this for all quantor
240      * @return a new {@code ForAll8} instance of 8 variables
241      */
242     public <T1, T2, T3, T4, T5, T6, T7, T8> ForAll8<T1, T2, T3, T4, T5, T6, T7, T8> forAll(Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6, Arbitrary<T7> a7, Arbitrary<T8> a8) {
243         return new ForAll8<>(name, a1, a2, a3, a4, a5, a6, a7, a8);
244     }
245 
246     /**
247      * Represents a logical for all quantor.
248      *
249      * @param <T1> 1st variable type of this for all quantor
250      * @author Daniel Dietrich
251      */
252     public static class ForAll1<T1> {
253 
254         private final String name;
255         private final Arbitrary<T1> a1;
256 
257         ForAll1(String name, Arbitrary<T1> a1) {
258             this.name = name;
259             this.a1 = a1;
260         }
261 
262         /**
263          * Returns a checkable property that checks values of the 1 variables of this {@code ForAll} quantor.
264          *
265          * @param predicate A 1-ary predicate
266          * @return a new {@code Property1} of 1 variables.
267          */
268         public Property1<T1> suchThat(CheckedFunction1<T1, Boolean> predicate) {
269             final CheckedFunction1<T1, Condition> proposition = (t1) -> new Condition(true, predicate.apply(t1));
270             return new Property1<>(name, a1, proposition);
271         }
272     }
273 
274     /**
275      * Represents a logical for all quantor.
276      *
277      * @param <T1> 1st variable type of this for all quantor
278      * @param <T2> 2nd variable type of this for all quantor
279      * @author Daniel Dietrich
280      */
281     public static class ForAll2<T1, T2> {
282 
283         private final String name;
284         private final Arbitrary<T1> a1;
285         private final Arbitrary<T2> a2;
286 
287         ForAll2(String name, Arbitrary<T1> a1, Arbitrary<T2> a2) {
288             this.name = name;
289             this.a1 = a1;
290             this.a2 = a2;
291         }
292 
293         /**
294          * Returns a checkable property that checks values of the 2 variables of this {@code ForAll} quantor.
295          *
296          * @param predicate A 2-ary predicate
297          * @return a new {@code Property2} of 2 variables.
298          */
299         public Property2<T1, T2> suchThat(CheckedFunction2<T1, T2, Boolean> predicate) {
300             final CheckedFunction2<T1, T2, Condition> proposition = (t1, t2) -> new Condition(true, predicate.apply(t1, t2));
301             return new Property2<>(name, a1, a2, proposition);
302         }
303     }
304 
305     /**
306      * Represents a logical for all quantor.
307      *
308      * @param <T1> 1st variable type of this for all quantor
309      * @param <T2> 2nd variable type of this for all quantor
310      * @param <T3> 3rd variable type of this for all quantor
311      * @author Daniel Dietrich
312      */
313     public static class ForAll3<T1, T2, T3> {
314 
315         private final String name;
316         private final Arbitrary<T1> a1;
317         private final Arbitrary<T2> a2;
318         private final Arbitrary<T3> a3;
319 
320         ForAll3(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3) {
321             this.name = name;
322             this.a1 = a1;
323             this.a2 = a2;
324             this.a3 = a3;
325         }
326 
327         /**
328          * Returns a checkable property that checks values of the 3 variables of this {@code ForAll} quantor.
329          *
330          * @param predicate A 3-ary predicate
331          * @return a new {@code Property3} of 3 variables.
332          */
333         public Property3<T1, T2, T3> suchThat(CheckedFunction3<T1, T2, T3, Boolean> predicate) {
334             final CheckedFunction3<T1, T2, T3, Condition> proposition = (t1, t2, t3) -> new Condition(true, predicate.apply(t1, t2, t3));
335             return new Property3<>(name, a1, a2, a3, proposition);
336         }
337     }
338 
339     /**
340      * Represents a logical for all quantor.
341      *
342      * @param <T1> 1st variable type of this for all quantor
343      * @param <T2> 2nd variable type of this for all quantor
344      * @param <T3> 3rd variable type of this for all quantor
345      * @param <T4> 4th variable type of this for all quantor
346      * @author Daniel Dietrich
347      */
348     public static class ForAll4<T1, T2, T3, T4> {
349 
350         private final String name;
351         private final Arbitrary<T1> a1;
352         private final Arbitrary<T2> a2;
353         private final Arbitrary<T3> a3;
354         private final Arbitrary<T4> a4;
355 
356         ForAll4(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4) {
357             this.name = name;
358             this.a1 = a1;
359             this.a2 = a2;
360             this.a3 = a3;
361             this.a4 = a4;
362         }
363 
364         /**
365          * Returns a checkable property that checks values of the 4 variables of this {@code ForAll} quantor.
366          *
367          * @param predicate A 4-ary predicate
368          * @return a new {@code Property4} of 4 variables.
369          */
370         public Property4<T1, T2, T3, T4> suchThat(CheckedFunction4<T1, T2, T3, T4, Boolean> predicate) {
371             final CheckedFunction4<T1, T2, T3, T4, Condition> proposition = (t1, t2, t3, t4) -> new Condition(true, predicate.apply(t1, t2, t3, t4));
372             return new Property4<>(name, a1, a2, a3, a4, proposition);
373         }
374     }
375 
376     /**
377      * Represents a logical for all quantor.
378      *
379      * @param <T1> 1st variable type of this for all quantor
380      * @param <T2> 2nd variable type of this for all quantor
381      * @param <T3> 3rd variable type of this for all quantor
382      * @param <T4> 4th variable type of this for all quantor
383      * @param <T5> 5th variable type of this for all quantor
384      * @author Daniel Dietrich
385      */
386     public static class ForAll5<T1, T2, T3, T4, T5> {
387 
388         private final String name;
389         private final Arbitrary<T1> a1;
390         private final Arbitrary<T2> a2;
391         private final Arbitrary<T3> a3;
392         private final Arbitrary<T4> a4;
393         private final Arbitrary<T5> a5;
394 
395         ForAll5(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5) {
396             this.name = name;
397             this.a1 = a1;
398             this.a2 = a2;
399             this.a3 = a3;
400             this.a4 = a4;
401             this.a5 = a5;
402         }
403 
404         /**
405          * Returns a checkable property that checks values of the 5 variables of this {@code ForAll} quantor.
406          *
407          * @param predicate A 5-ary predicate
408          * @return a new {@code Property5} of 5 variables.
409          */
410         public Property5<T1, T2, T3, T4, T5> suchThat(CheckedFunction5<T1, T2, T3, T4, T5, Boolean> predicate) {
411             final CheckedFunction5<T1, T2, T3, T4, T5, Condition> proposition = (t1, t2, t3, t4, t5) -> new Condition(true, predicate.apply(t1, t2, t3, t4, t5));
412             return new Property5<>(name, a1, a2, a3, a4, a5, proposition);
413         }
414     }
415 
416     /**
417      * Represents a logical for all quantor.
418      *
419      * @param <T1> 1st variable type of this for all quantor
420      * @param <T2> 2nd variable type of this for all quantor
421      * @param <T3> 3rd variable type of this for all quantor
422      * @param <T4> 4th variable type of this for all quantor
423      * @param <T5> 5th variable type of this for all quantor
424      * @param <T6> 6th variable type of this for all quantor
425      * @author Daniel Dietrich
426      */
427     public static class ForAll6<T1, T2, T3, T4, T5, T6> {
428 
429         private final String name;
430         private final Arbitrary<T1> a1;
431         private final Arbitrary<T2> a2;
432         private final Arbitrary<T3> a3;
433         private final Arbitrary<T4> a4;
434         private final Arbitrary<T5> a5;
435         private final Arbitrary<T6> a6;
436 
437         ForAll6(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6) {
438             this.name = name;
439             this.a1 = a1;
440             this.a2 = a2;
441             this.a3 = a3;
442             this.a4 = a4;
443             this.a5 = a5;
444             this.a6 = a6;
445         }
446 
447         /**
448          * Returns a checkable property that checks values of the 6 variables of this {@code ForAll} quantor.
449          *
450          * @param predicate A 6-ary predicate
451          * @return a new {@code Property6} of 6 variables.
452          */
453         public Property6<T1, T2, T3, T4, T5, T6> suchThat(CheckedFunction6<T1, T2, T3, T4, T5, T6, Boolean> predicate) {
454             final CheckedFunction6<T1, T2, T3, T4, T5, T6, Condition> proposition = (t1, t2, t3, t4, t5, t6) -> new Condition(true, predicate.apply(t1, t2, t3, t4, t5, t6));
455             return new Property6<>(name, a1, a2, a3, a4, a5, a6, proposition);
456         }
457     }
458 
459     /**
460      * Represents a logical for all quantor.
461      *
462      * @param <T1> 1st variable type of this for all quantor
463      * @param <T2> 2nd variable type of this for all quantor
464      * @param <T3> 3rd variable type of this for all quantor
465      * @param <T4> 4th variable type of this for all quantor
466      * @param <T5> 5th variable type of this for all quantor
467      * @param <T6> 6th variable type of this for all quantor
468      * @param <T7> 7th variable type of this for all quantor
469      * @author Daniel Dietrich
470      */
471     public static class ForAll7<T1, T2, T3, T4, T5, T6, T7> {
472 
473         private final String name;
474         private final Arbitrary<T1> a1;
475         private final Arbitrary<T2> a2;
476         private final Arbitrary<T3> a3;
477         private final Arbitrary<T4> a4;
478         private final Arbitrary<T5> a5;
479         private final Arbitrary<T6> a6;
480         private final Arbitrary<T7> a7;
481 
482         ForAll7(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6, Arbitrary<T7> a7) {
483             this.name = name;
484             this.a1 = a1;
485             this.a2 = a2;
486             this.a3 = a3;
487             this.a4 = a4;
488             this.a5 = a5;
489             this.a6 = a6;
490             this.a7 = a7;
491         }
492 
493         /**
494          * Returns a checkable property that checks values of the 7 variables of this {@code ForAll} quantor.
495          *
496          * @param predicate A 7-ary predicate
497          * @return a new {@code Property7} of 7 variables.
498          */
499         public Property7<T1, T2, T3, T4, T5, T6, T7> suchThat(CheckedFunction7<T1, T2, T3, T4, T5, T6, T7, Boolean> predicate) {
500             final CheckedFunction7<T1, T2, T3, T4, T5, T6, T7, Condition> proposition = (t1, t2, t3, t4, t5, t6, t7) -> new Condition(true, predicate.apply(t1, t2, t3, t4, t5, t6, t7));
501             return new Property7<>(name, a1, a2, a3, a4, a5, a6, a7, proposition);
502         }
503     }
504 
505     /**
506      * Represents a logical for all quantor.
507      *
508      * @param <T1> 1st variable type of this for all quantor
509      * @param <T2> 2nd variable type of this for all quantor
510      * @param <T3> 3rd variable type of this for all quantor
511      * @param <T4> 4th variable type of this for all quantor
512      * @param <T5> 5th variable type of this for all quantor
513      * @param <T6> 6th variable type of this for all quantor
514      * @param <T7> 7th variable type of this for all quantor
515      * @param <T8> 8th variable type of this for all quantor
516      * @author Daniel Dietrich
517      */
518     public static class ForAll8<T1, T2, T3, T4, T5, T6, T7, T8> {
519 
520         private final String name;
521         private final Arbitrary<T1> a1;
522         private final Arbitrary<T2> a2;
523         private final Arbitrary<T3> a3;
524         private final Arbitrary<T4> a4;
525         private final Arbitrary<T5> a5;
526         private final Arbitrary<T6> a6;
527         private final Arbitrary<T7> a7;
528         private final Arbitrary<T8> a8;
529 
530         ForAll8(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6, Arbitrary<T7> a7, Arbitrary<T8> a8) {
531             this.name = name;
532             this.a1 = a1;
533             this.a2 = a2;
534             this.a3 = a3;
535             this.a4 = a4;
536             this.a5 = a5;
537             this.a6 = a6;
538             this.a7 = a7;
539             this.a8 = a8;
540         }
541 
542         /**
543          * Returns a checkable property that checks values of the 8 variables of this {@code ForAll} quantor.
544          *
545          * @param predicate A 8-ary predicate
546          * @return a new {@code Property8} of 8 variables.
547          */
548         public Property8<T1, T2, T3, T4, T5, T6, T7, T8> suchThat(CheckedFunction8<T1, T2, T3, T4, T5, T6, T7, T8, Boolean> predicate) {
549             final CheckedFunction8<T1, T2, T3, T4, T5, T6, T7, T8, Condition> proposition = (t1, t2, t3, t4, t5, t6, t7, t8) -> new Condition(true, predicate.apply(t1, t2, t3, t4, t5, t6, t7, t8));
550             return new Property8<>(name, a1, a2, a3, a4, a5, a6, a7, a8, proposition);
551         }
552     }
553 
554     /**
555      * Represents a 1-ary checkable property.
556      *
557      * @author Daniel Dietrich
558      */
559     public static class Property1<T1> implements Checkable {
560 
561         private final String name;
562         private final Arbitrary<T1> a1;
563         private final CheckedFunction1<T1, Condition> predicate;
564 
565         Property1(String name, Arbitrary<T1> a1, CheckedFunction1<T1, Condition> predicate) {
566             this.name = name;
567             this.a1 = a1;
568             this.predicate = predicate;
569         }
570 
571         /**
572          * Returns an implication which composes this Property as pre-condition and a given post-condition.
573          *
574          * @param postcondition The postcondition of this implication
575          * @return A new Checkable implication
576          */
577         public Checkable implies(CheckedFunction1<T1, Boolean> postcondition) {
578             final CheckedFunction1<T1, Condition> implication = (t1) -> {
579                 final Condition precondition = predicate.apply(t1);
580                 if (precondition.isFalse()) {
581                     return Condition.EX_FALSO_QUODLIBET;
582                 } else {
583                     return new Condition(true, postcondition.apply(t1));
584                 }
585             };
586             return new Property1<>(name, a1, implication);
587         }
588 
589         @Override
590         public CheckResult check(Random random, int size, int tries) {
591             Objects.requireNonNull(random, "random is null");
592             if (tries < 0) {
593                 throw new IllegalArgumentException("tries < 0");
594             }
595             final long startTime = System.currentTimeMillis();
596             try {
597                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
598                 boolean exhausted = true;
599                 for (int i = 1; i <= tries; i++) {
600                     try {
601                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
602                         try {
603                             final Condition condition = Try.of(() -> predicate.apply(val1)).recover(x -> { throw predicateError(x); }).get();
604                             if (condition.precondition) {
605                                 exhausted = false;
606                                 if (!condition.postcondition) {
607                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
608                                     return new CheckResult.Falsified(name, i, Tuple.of(val1));
609                                 }
610                             }
611                         } catch(CheckError err) {
612                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
613                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1)));
614                         }
615                     } catch(CheckError err) {
616                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
617                         return new CheckResult.Erroneous(name, i, err, Option.none());
618                     }
619                 }
620                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
621                 return new CheckResult.Satisfied(name, tries, exhausted);
622             } catch(CheckError err) {
623                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
624                 return new CheckResult.Erroneous(name, 0, err, Option.none());
625             }
626         }
627     }
628 
629     /**
630      * Represents a 2-ary checkable property.
631      *
632      * @author Daniel Dietrich
633      */
634     public static class Property2<T1, T2> implements Checkable {
635 
636         private final String name;
637         private final Arbitrary<T1> a1;
638         private final Arbitrary<T2> a2;
639         private final CheckedFunction2<T1, T2, Condition> predicate;
640 
641         Property2(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, CheckedFunction2<T1, T2, Condition> predicate) {
642             this.name = name;
643             this.a1 = a1;
644             this.a2 = a2;
645             this.predicate = predicate;
646         }
647 
648         /**
649          * Returns an implication which composes this Property as pre-condition and a given post-condition.
650          *
651          * @param postcondition The postcondition of this implication
652          * @return A new Checkable implication
653          */
654         public Checkable implies(CheckedFunction2<T1, T2, Boolean> postcondition) {
655             final CheckedFunction2<T1, T2, Condition> implication = (t1, t2) -> {
656                 final Condition precondition = predicate.apply(t1, t2);
657                 if (precondition.isFalse()) {
658                     return Condition.EX_FALSO_QUODLIBET;
659                 } else {
660                     return new Condition(true, postcondition.apply(t1, t2));
661                 }
662             };
663             return new Property2<>(name, a1, a2, implication);
664         }
665 
666         @Override
667         public CheckResult check(Random random, int size, int tries) {
668             Objects.requireNonNull(random, "random is null");
669             if (tries < 0) {
670                 throw new IllegalArgumentException("tries < 0");
671             }
672             final long startTime = System.currentTimeMillis();
673             try {
674                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
675                 final Gen<T2> gen2 = Try.of(() -> a2.apply(size)).recover(x -> { throw arbitraryError(2, size, x); }).get();
676                 boolean exhausted = true;
677                 for (int i = 1; i <= tries; i++) {
678                     try {
679                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
680                         final T2 val2 = Try.of(() -> gen2.apply(random)).recover(x -> { throw genError(2, size, x); }).get();
681                         try {
682                             final Condition condition = Try.of(() -> predicate.apply(val1, val2)).recover(x -> { throw predicateError(x); }).get();
683                             if (condition.precondition) {
684                                 exhausted = false;
685                                 if (!condition.postcondition) {
686                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
687                                     return new CheckResult.Falsified(name, i, Tuple.of(val1, val2));
688                                 }
689                             }
690                         } catch(CheckError err) {
691                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
692                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1, val2)));
693                         }
694                     } catch(CheckError err) {
695                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
696                         return new CheckResult.Erroneous(name, i, err, Option.none());
697                     }
698                 }
699                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
700                 return new CheckResult.Satisfied(name, tries, exhausted);
701             } catch(CheckError err) {
702                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
703                 return new CheckResult.Erroneous(name, 0, err, Option.none());
704             }
705         }
706     }
707 
708     /**
709      * Represents a 3-ary checkable property.
710      *
711      * @author Daniel Dietrich
712      */
713     public static class Property3<T1, T2, T3> implements Checkable {
714 
715         private final String name;
716         private final Arbitrary<T1> a1;
717         private final Arbitrary<T2> a2;
718         private final Arbitrary<T3> a3;
719         private final CheckedFunction3<T1, T2, T3, Condition> predicate;
720 
721         Property3(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, CheckedFunction3<T1, T2, T3, Condition> predicate) {
722             this.name = name;
723             this.a1 = a1;
724             this.a2 = a2;
725             this.a3 = a3;
726             this.predicate = predicate;
727         }
728 
729         /**
730          * Returns an implication which composes this Property as pre-condition and a given post-condition.
731          *
732          * @param postcondition The postcondition of this implication
733          * @return A new Checkable implication
734          */
735         public Checkable implies(CheckedFunction3<T1, T2, T3, Boolean> postcondition) {
736             final CheckedFunction3<T1, T2, T3, Condition> implication = (t1, t2, t3) -> {
737                 final Condition precondition = predicate.apply(t1, t2, t3);
738                 if (precondition.isFalse()) {
739                     return Condition.EX_FALSO_QUODLIBET;
740                 } else {
741                     return new Condition(true, postcondition.apply(t1, t2, t3));
742                 }
743             };
744             return new Property3<>(name, a1, a2, a3, implication);
745         }
746 
747         @Override
748         public CheckResult check(Random random, int size, int tries) {
749             Objects.requireNonNull(random, "random is null");
750             if (tries < 0) {
751                 throw new IllegalArgumentException("tries < 0");
752             }
753             final long startTime = System.currentTimeMillis();
754             try {
755                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
756                 final Gen<T2> gen2 = Try.of(() -> a2.apply(size)).recover(x -> { throw arbitraryError(2, size, x); }).get();
757                 final Gen<T3> gen3 = Try.of(() -> a3.apply(size)).recover(x -> { throw arbitraryError(3, size, x); }).get();
758                 boolean exhausted = true;
759                 for (int i = 1; i <= tries; i++) {
760                     try {
761                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
762                         final T2 val2 = Try.of(() -> gen2.apply(random)).recover(x -> { throw genError(2, size, x); }).get();
763                         final T3 val3 = Try.of(() -> gen3.apply(random)).recover(x -> { throw genError(3, size, x); }).get();
764                         try {
765                             final Condition condition = Try.of(() -> predicate.apply(val1, val2, val3)).recover(x -> { throw predicateError(x); }).get();
766                             if (condition.precondition) {
767                                 exhausted = false;
768                                 if (!condition.postcondition) {
769                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
770                                     return new CheckResult.Falsified(name, i, Tuple.of(val1, val2, val3));
771                                 }
772                             }
773                         } catch(CheckError err) {
774                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
775                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1, val2, val3)));
776                         }
777                     } catch(CheckError err) {
778                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
779                         return new CheckResult.Erroneous(name, i, err, Option.none());
780                     }
781                 }
782                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
783                 return new CheckResult.Satisfied(name, tries, exhausted);
784             } catch(CheckError err) {
785                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
786                 return new CheckResult.Erroneous(name, 0, err, Option.none());
787             }
788         }
789     }
790 
791     /**
792      * Represents a 4-ary checkable property.
793      *
794      * @author Daniel Dietrich
795      */
796     public static class Property4<T1, T2, T3, T4> implements Checkable {
797 
798         private final String name;
799         private final Arbitrary<T1> a1;
800         private final Arbitrary<T2> a2;
801         private final Arbitrary<T3> a3;
802         private final Arbitrary<T4> a4;
803         private final CheckedFunction4<T1, T2, T3, T4, Condition> predicate;
804 
805         Property4(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, CheckedFunction4<T1, T2, T3, T4, Condition> predicate) {
806             this.name = name;
807             this.a1 = a1;
808             this.a2 = a2;
809             this.a3 = a3;
810             this.a4 = a4;
811             this.predicate = predicate;
812         }
813 
814         /**
815          * Returns an implication which composes this Property as pre-condition and a given post-condition.
816          *
817          * @param postcondition The postcondition of this implication
818          * @return A new Checkable implication
819          */
820         public Checkable implies(CheckedFunction4<T1, T2, T3, T4, Boolean> postcondition) {
821             final CheckedFunction4<T1, T2, T3, T4, Condition> implication = (t1, t2, t3, t4) -> {
822                 final Condition precondition = predicate.apply(t1, t2, t3, t4);
823                 if (precondition.isFalse()) {
824                     return Condition.EX_FALSO_QUODLIBET;
825                 } else {
826                     return new Condition(true, postcondition.apply(t1, t2, t3, t4));
827                 }
828             };
829             return new Property4<>(name, a1, a2, a3, a4, implication);
830         }
831 
832         @Override
833         public CheckResult check(Random random, int size, int tries) {
834             Objects.requireNonNull(random, "random is null");
835             if (tries < 0) {
836                 throw new IllegalArgumentException("tries < 0");
837             }
838             final long startTime = System.currentTimeMillis();
839             try {
840                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
841                 final Gen<T2> gen2 = Try.of(() -> a2.apply(size)).recover(x -> { throw arbitraryError(2, size, x); }).get();
842                 final Gen<T3> gen3 = Try.of(() -> a3.apply(size)).recover(x -> { throw arbitraryError(3, size, x); }).get();
843                 final Gen<T4> gen4 = Try.of(() -> a4.apply(size)).recover(x -> { throw arbitraryError(4, size, x); }).get();
844                 boolean exhausted = true;
845                 for (int i = 1; i <= tries; i++) {
846                     try {
847                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
848                         final T2 val2 = Try.of(() -> gen2.apply(random)).recover(x -> { throw genError(2, size, x); }).get();
849                         final T3 val3 = Try.of(() -> gen3.apply(random)).recover(x -> { throw genError(3, size, x); }).get();
850                         final T4 val4 = Try.of(() -> gen4.apply(random)).recover(x -> { throw genError(4, size, x); }).get();
851                         try {
852                             final Condition condition = Try.of(() -> predicate.apply(val1, val2, val3, val4)).recover(x -> { throw predicateError(x); }).get();
853                             if (condition.precondition) {
854                                 exhausted = false;
855                                 if (!condition.postcondition) {
856                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
857                                     return new CheckResult.Falsified(name, i, Tuple.of(val1, val2, val3, val4));
858                                 }
859                             }
860                         } catch(CheckError err) {
861                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
862                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1, val2, val3, val4)));
863                         }
864                     } catch(CheckError err) {
865                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
866                         return new CheckResult.Erroneous(name, i, err, Option.none());
867                     }
868                 }
869                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
870                 return new CheckResult.Satisfied(name, tries, exhausted);
871             } catch(CheckError err) {
872                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
873                 return new CheckResult.Erroneous(name, 0, err, Option.none());
874             }
875         }
876     }
877 
878     /**
879      * Represents a 5-ary checkable property.
880      *
881      * @author Daniel Dietrich
882      */
883     public static class Property5<T1, T2, T3, T4, T5> implements Checkable {
884 
885         private final String name;
886         private final Arbitrary<T1> a1;
887         private final Arbitrary<T2> a2;
888         private final Arbitrary<T3> a3;
889         private final Arbitrary<T4> a4;
890         private final Arbitrary<T5> a5;
891         private final CheckedFunction5<T1, T2, T3, T4, T5, Condition> predicate;
892 
893         Property5(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, CheckedFunction5<T1, T2, T3, T4, T5, Condition> predicate) {
894             this.name = name;
895             this.a1 = a1;
896             this.a2 = a2;
897             this.a3 = a3;
898             this.a4 = a4;
899             this.a5 = a5;
900             this.predicate = predicate;
901         }
902 
903         /**
904          * Returns an implication which composes this Property as pre-condition and a given post-condition.
905          *
906          * @param postcondition The postcondition of this implication
907          * @return A new Checkable implication
908          */
909         public Checkable implies(CheckedFunction5<T1, T2, T3, T4, T5, Boolean> postcondition) {
910             final CheckedFunction5<T1, T2, T3, T4, T5, Condition> implication = (t1, t2, t3, t4, t5) -> {
911                 final Condition precondition = predicate.apply(t1, t2, t3, t4, t5);
912                 if (precondition.isFalse()) {
913                     return Condition.EX_FALSO_QUODLIBET;
914                 } else {
915                     return new Condition(true, postcondition.apply(t1, t2, t3, t4, t5));
916                 }
917             };
918             return new Property5<>(name, a1, a2, a3, a4, a5, implication);
919         }
920 
921         @Override
922         public CheckResult check(Random random, int size, int tries) {
923             Objects.requireNonNull(random, "random is null");
924             if (tries < 0) {
925                 throw new IllegalArgumentException("tries < 0");
926             }
927             final long startTime = System.currentTimeMillis();
928             try {
929                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
930                 final Gen<T2> gen2 = Try.of(() -> a2.apply(size)).recover(x -> { throw arbitraryError(2, size, x); }).get();
931                 final Gen<T3> gen3 = Try.of(() -> a3.apply(size)).recover(x -> { throw arbitraryError(3, size, x); }).get();
932                 final Gen<T4> gen4 = Try.of(() -> a4.apply(size)).recover(x -> { throw arbitraryError(4, size, x); }).get();
933                 final Gen<T5> gen5 = Try.of(() -> a5.apply(size)).recover(x -> { throw arbitraryError(5, size, x); }).get();
934                 boolean exhausted = true;
935                 for (int i = 1; i <= tries; i++) {
936                     try {
937                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
938                         final T2 val2 = Try.of(() -> gen2.apply(random)).recover(x -> { throw genError(2, size, x); }).get();
939                         final T3 val3 = Try.of(() -> gen3.apply(random)).recover(x -> { throw genError(3, size, x); }).get();
940                         final T4 val4 = Try.of(() -> gen4.apply(random)).recover(x -> { throw genError(4, size, x); }).get();
941                         final T5 val5 = Try.of(() -> gen5.apply(random)).recover(x -> { throw genError(5, size, x); }).get();
942                         try {
943                             final Condition condition = Try.of(() -> predicate.apply(val1, val2, val3, val4, val5)).recover(x -> { throw predicateError(x); }).get();
944                             if (condition.precondition) {
945                                 exhausted = false;
946                                 if (!condition.postcondition) {
947                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
948                                     return new CheckResult.Falsified(name, i, Tuple.of(val1, val2, val3, val4, val5));
949                                 }
950                             }
951                         } catch(CheckError err) {
952                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
953                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1, val2, val3, val4, val5)));
954                         }
955                     } catch(CheckError err) {
956                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
957                         return new CheckResult.Erroneous(name, i, err, Option.none());
958                     }
959                 }
960                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
961                 return new CheckResult.Satisfied(name, tries, exhausted);
962             } catch(CheckError err) {
963                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
964                 return new CheckResult.Erroneous(name, 0, err, Option.none());
965             }
966         }
967     }
968 
969     /**
970      * Represents a 6-ary checkable property.
971      *
972      * @author Daniel Dietrich
973      */
974     public static class Property6<T1, T2, T3, T4, T5, T6> implements Checkable {
975 
976         private final String name;
977         private final Arbitrary<T1> a1;
978         private final Arbitrary<T2> a2;
979         private final Arbitrary<T3> a3;
980         private final Arbitrary<T4> a4;
981         private final Arbitrary<T5> a5;
982         private final Arbitrary<T6> a6;
983         private final CheckedFunction6<T1, T2, T3, T4, T5, T6, Condition> predicate;
984 
985         Property6(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6, CheckedFunction6<T1, T2, T3, T4, T5, T6, Condition> predicate) {
986             this.name = name;
987             this.a1 = a1;
988             this.a2 = a2;
989             this.a3 = a3;
990             this.a4 = a4;
991             this.a5 = a5;
992             this.a6 = a6;
993             this.predicate = predicate;
994         }
995 
996         /**
997          * Returns an implication which composes this Property as pre-condition and a given post-condition.
998          *
999          * @param postcondition The postcondition of this implication
1000          * @return A new Checkable implication
1001          */
1002         public Checkable implies(CheckedFunction6<T1, T2, T3, T4, T5, T6, Boolean> postcondition) {
1003             final CheckedFunction6<T1, T2, T3, T4, T5, T6, Condition> implication = (t1, t2, t3, t4, t5, t6) -> {
1004                 final Condition precondition = predicate.apply(t1, t2, t3, t4, t5, t6);
1005                 if (precondition.isFalse()) {
1006                     return Condition.EX_FALSO_QUODLIBET;
1007                 } else {
1008                     return new Condition(true, postcondition.apply(t1, t2, t3, t4, t5, t6));
1009                 }
1010             };
1011             return new Property6<>(name, a1, a2, a3, a4, a5, a6, implication);
1012         }
1013 
1014         @Override
1015         public CheckResult check(Random random, int size, int tries) {
1016             Objects.requireNonNull(random, "random is null");
1017             if (tries < 0) {
1018                 throw new IllegalArgumentException("tries < 0");
1019             }
1020             final long startTime = System.currentTimeMillis();
1021             try {
1022                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
1023                 final Gen<T2> gen2 = Try.of(() -> a2.apply(size)).recover(x -> { throw arbitraryError(2, size, x); }).get();
1024                 final Gen<T3> gen3 = Try.of(() -> a3.apply(size)).recover(x -> { throw arbitraryError(3, size, x); }).get();
1025                 final Gen<T4> gen4 = Try.of(() -> a4.apply(size)).recover(x -> { throw arbitraryError(4, size, x); }).get();
1026                 final Gen<T5> gen5 = Try.of(() -> a5.apply(size)).recover(x -> { throw arbitraryError(5, size, x); }).get();
1027                 final Gen<T6> gen6 = Try.of(() -> a6.apply(size)).recover(x -> { throw arbitraryError(6, size, x); }).get();
1028                 boolean exhausted = true;
1029                 for (int i = 1; i <= tries; i++) {
1030                     try {
1031                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
1032                         final T2 val2 = Try.of(() -> gen2.apply(random)).recover(x -> { throw genError(2, size, x); }).get();
1033                         final T3 val3 = Try.of(() -> gen3.apply(random)).recover(x -> { throw genError(3, size, x); }).get();
1034                         final T4 val4 = Try.of(() -> gen4.apply(random)).recover(x -> { throw genError(4, size, x); }).get();
1035                         final T5 val5 = Try.of(() -> gen5.apply(random)).recover(x -> { throw genError(5, size, x); }).get();
1036                         final T6 val6 = Try.of(() -> gen6.apply(random)).recover(x -> { throw genError(6, size, x); }).get();
1037                         try {
1038                             final Condition condition = Try.of(() -> predicate.apply(val1, val2, val3, val4, val5, val6)).recover(x -> { throw predicateError(x); }).get();
1039                             if (condition.precondition) {
1040                                 exhausted = false;
1041                                 if (!condition.postcondition) {
1042                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
1043                                     return new CheckResult.Falsified(name, i, Tuple.of(val1, val2, val3, val4, val5, val6));
1044                                 }
1045                             }
1046                         } catch(CheckError err) {
1047                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
1048                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1, val2, val3, val4, val5, val6)));
1049                         }
1050                     } catch(CheckError err) {
1051                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
1052                         return new CheckResult.Erroneous(name, i, err, Option.none());
1053                     }
1054                 }
1055                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
1056                 return new CheckResult.Satisfied(name, tries, exhausted);
1057             } catch(CheckError err) {
1058                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
1059                 return new CheckResult.Erroneous(name, 0, err, Option.none());
1060             }
1061         }
1062     }
1063 
1064     /**
1065      * Represents a 7-ary checkable property.
1066      *
1067      * @author Daniel Dietrich
1068      */
1069     public static class Property7<T1, T2, T3, T4, T5, T6, T7> implements Checkable {
1070 
1071         private final String name;
1072         private final Arbitrary<T1> a1;
1073         private final Arbitrary<T2> a2;
1074         private final Arbitrary<T3> a3;
1075         private final Arbitrary<T4> a4;
1076         private final Arbitrary<T5> a5;
1077         private final Arbitrary<T6> a6;
1078         private final Arbitrary<T7> a7;
1079         private final CheckedFunction7<T1, T2, T3, T4, T5, T6, T7, Condition> predicate;
1080 
1081         Property7(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6, Arbitrary<T7> a7, CheckedFunction7<T1, T2, T3, T4, T5, T6, T7, Condition> predicate) {
1082             this.name = name;
1083             this.a1 = a1;
1084             this.a2 = a2;
1085             this.a3 = a3;
1086             this.a4 = a4;
1087             this.a5 = a5;
1088             this.a6 = a6;
1089             this.a7 = a7;
1090             this.predicate = predicate;
1091         }
1092 
1093         /**
1094          * Returns an implication which composes this Property as pre-condition and a given post-condition.
1095          *
1096          * @param postcondition The postcondition of this implication
1097          * @return A new Checkable implication
1098          */
1099         public Checkable implies(CheckedFunction7<T1, T2, T3, T4, T5, T6, T7, Boolean> postcondition) {
1100             final CheckedFunction7<T1, T2, T3, T4, T5, T6, T7, Condition> implication = (t1, t2, t3, t4, t5, t6, t7) -> {
1101                 final Condition precondition = predicate.apply(t1, t2, t3, t4, t5, t6, t7);
1102                 if (precondition.isFalse()) {
1103                     return Condition.EX_FALSO_QUODLIBET;
1104                 } else {
1105                     return new Condition(true, postcondition.apply(t1, t2, t3, t4, t5, t6, t7));
1106                 }
1107             };
1108             return new Property7<>(name, a1, a2, a3, a4, a5, a6, a7, implication);
1109         }
1110 
1111         @Override
1112         public CheckResult check(Random random, int size, int tries) {
1113             Objects.requireNonNull(random, "random is null");
1114             if (tries < 0) {
1115                 throw new IllegalArgumentException("tries < 0");
1116             }
1117             final long startTime = System.currentTimeMillis();
1118             try {
1119                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
1120                 final Gen<T2> gen2 = Try.of(() -> a2.apply(size)).recover(x -> { throw arbitraryError(2, size, x); }).get();
1121                 final Gen<T3> gen3 = Try.of(() -> a3.apply(size)).recover(x -> { throw arbitraryError(3, size, x); }).get();
1122                 final Gen<T4> gen4 = Try.of(() -> a4.apply(size)).recover(x -> { throw arbitraryError(4, size, x); }).get();
1123                 final Gen<T5> gen5 = Try.of(() -> a5.apply(size)).recover(x -> { throw arbitraryError(5, size, x); }).get();
1124                 final Gen<T6> gen6 = Try.of(() -> a6.apply(size)).recover(x -> { throw arbitraryError(6, size, x); }).get();
1125                 final Gen<T7> gen7 = Try.of(() -> a7.apply(size)).recover(x -> { throw arbitraryError(7, size, x); }).get();
1126                 boolean exhausted = true;
1127                 for (int i = 1; i <= tries; i++) {
1128                     try {
1129                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
1130                         final T2 val2 = Try.of(() -> gen2.apply(random)).recover(x -> { throw genError(2, size, x); }).get();
1131                         final T3 val3 = Try.of(() -> gen3.apply(random)).recover(x -> { throw genError(3, size, x); }).get();
1132                         final T4 val4 = Try.of(() -> gen4.apply(random)).recover(x -> { throw genError(4, size, x); }).get();
1133                         final T5 val5 = Try.of(() -> gen5.apply(random)).recover(x -> { throw genError(5, size, x); }).get();
1134                         final T6 val6 = Try.of(() -> gen6.apply(random)).recover(x -> { throw genError(6, size, x); }).get();
1135                         final T7 val7 = Try.of(() -> gen7.apply(random)).recover(x -> { throw genError(7, size, x); }).get();
1136                         try {
1137                             final Condition condition = Try.of(() -> predicate.apply(val1, val2, val3, val4, val5, val6, val7)).recover(x -> { throw predicateError(x); }).get();
1138                             if (condition.precondition) {
1139                                 exhausted = false;
1140                                 if (!condition.postcondition) {
1141                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
1142                                     return new CheckResult.Falsified(name, i, Tuple.of(val1, val2, val3, val4, val5, val6, val7));
1143                                 }
1144                             }
1145                         } catch(CheckError err) {
1146                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
1147                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1, val2, val3, val4, val5, val6, val7)));
1148                         }
1149                     } catch(CheckError err) {
1150                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
1151                         return new CheckResult.Erroneous(name, i, err, Option.none());
1152                     }
1153                 }
1154                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
1155                 return new CheckResult.Satisfied(name, tries, exhausted);
1156             } catch(CheckError err) {
1157                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
1158                 return new CheckResult.Erroneous(name, 0, err, Option.none());
1159             }
1160         }
1161     }
1162 
1163     /**
1164      * Represents a 8-ary checkable property.
1165      *
1166      * @author Daniel Dietrich
1167      */
1168     public static class Property8<T1, T2, T3, T4, T5, T6, T7, T8> implements Checkable {
1169 
1170         private final String name;
1171         private final Arbitrary<T1> a1;
1172         private final Arbitrary<T2> a2;
1173         private final Arbitrary<T3> a3;
1174         private final Arbitrary<T4> a4;
1175         private final Arbitrary<T5> a5;
1176         private final Arbitrary<T6> a6;
1177         private final Arbitrary<T7> a7;
1178         private final Arbitrary<T8> a8;
1179         private final CheckedFunction8<T1, T2, T3, T4, T5, T6, T7, T8, Condition> predicate;
1180 
1181         Property8(String name, Arbitrary<T1> a1, Arbitrary<T2> a2, Arbitrary<T3> a3, Arbitrary<T4> a4, Arbitrary<T5> a5, Arbitrary<T6> a6, Arbitrary<T7> a7, Arbitrary<T8> a8, CheckedFunction8<T1, T2, T3, T4, T5, T6, T7, T8, Condition> predicate) {
1182             this.name = name;
1183             this.a1 = a1;
1184             this.a2 = a2;
1185             this.a3 = a3;
1186             this.a4 = a4;
1187             this.a5 = a5;
1188             this.a6 = a6;
1189             this.a7 = a7;
1190             this.a8 = a8;
1191             this.predicate = predicate;
1192         }
1193 
1194         /**
1195          * Returns an implication which composes this Property as pre-condition and a given post-condition.
1196          *
1197          * @param postcondition The postcondition of this implication
1198          * @return A new Checkable implication
1199          */
1200         public Checkable implies(CheckedFunction8<T1, T2, T3, T4, T5, T6, T7, T8, Boolean> postcondition) {
1201             final CheckedFunction8<T1, T2, T3, T4, T5, T6, T7, T8, Condition> implication = (t1, t2, t3, t4, t5, t6, t7, t8) -> {
1202                 final Condition precondition = predicate.apply(t1, t2, t3, t4, t5, t6, t7, t8);
1203                 if (precondition.isFalse()) {
1204                     return Condition.EX_FALSO_QUODLIBET;
1205                 } else {
1206                     return new Condition(true, postcondition.apply(t1, t2, t3, t4, t5, t6, t7, t8));
1207                 }
1208             };
1209             return new Property8<>(name, a1, a2, a3, a4, a5, a6, a7, a8, implication);
1210         }
1211 
1212         @Override
1213         public CheckResult check(Random random, int size, int tries) {
1214             Objects.requireNonNull(random, "random is null");
1215             if (tries < 0) {
1216                 throw new IllegalArgumentException("tries < 0");
1217             }
1218             final long startTime = System.currentTimeMillis();
1219             try {
1220                 final Gen<T1> gen1 = Try.of(() -> a1.apply(size)).recover(x -> { throw arbitraryError(1, size, x); }).get();
1221                 final Gen<T2> gen2 = Try.of(() -> a2.apply(size)).recover(x -> { throw arbitraryError(2, size, x); }).get();
1222                 final Gen<T3> gen3 = Try.of(() -> a3.apply(size)).recover(x -> { throw arbitraryError(3, size, x); }).get();
1223                 final Gen<T4> gen4 = Try.of(() -> a4.apply(size)).recover(x -> { throw arbitraryError(4, size, x); }).get();
1224                 final Gen<T5> gen5 = Try.of(() -> a5.apply(size)).recover(x -> { throw arbitraryError(5, size, x); }).get();
1225                 final Gen<T6> gen6 = Try.of(() -> a6.apply(size)).recover(x -> { throw arbitraryError(6, size, x); }).get();
1226                 final Gen<T7> gen7 = Try.of(() -> a7.apply(size)).recover(x -> { throw arbitraryError(7, size, x); }).get();
1227                 final Gen<T8> gen8 = Try.of(() -> a8.apply(size)).recover(x -> { throw arbitraryError(8, size, x); }).get();
1228                 boolean exhausted = true;
1229                 for (int i = 1; i <= tries; i++) {
1230                     try {
1231                         final T1 val1 = Try.of(() -> gen1.apply(random)).recover(x -> { throw genError(1, size, x); }).get();
1232                         final T2 val2 = Try.of(() -> gen2.apply(random)).recover(x -> { throw genError(2, size, x); }).get();
1233                         final T3 val3 = Try.of(() -> gen3.apply(random)).recover(x -> { throw genError(3, size, x); }).get();
1234                         final T4 val4 = Try.of(() -> gen4.apply(random)).recover(x -> { throw genError(4, size, x); }).get();
1235                         final T5 val5 = Try.of(() -> gen5.apply(random)).recover(x -> { throw genError(5, size, x); }).get();
1236                         final T6 val6 = Try.of(() -> gen6.apply(random)).recover(x -> { throw genError(6, size, x); }).get();
1237                         final T7 val7 = Try.of(() -> gen7.apply(random)).recover(x -> { throw genError(7, size, x); }).get();
1238                         final T8 val8 = Try.of(() -> gen8.apply(random)).recover(x -> { throw genError(8, size, x); }).get();
1239                         try {
1240                             final Condition condition = Try.of(() -> predicate.apply(val1, val2, val3, val4, val5, val6, val7, val8)).recover(x -> { throw predicateError(x); }).get();
1241                             if (condition.precondition) {
1242                                 exhausted = false;
1243                                 if (!condition.postcondition) {
1244                                     logFalsified(name, i, System.currentTimeMillis() - startTime);
1245                                     return new CheckResult.Falsified(name, i, Tuple.of(val1, val2, val3, val4, val5, val6, val7, val8));
1246                                 }
1247                             }
1248                         } catch(CheckError err) {
1249                             logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
1250                             return new CheckResult.Erroneous(name, i, err, Option.some(Tuple.of(val1, val2, val3, val4, val5, val6, val7, val8)));
1251                         }
1252                     } catch(CheckError err) {
1253                         logErroneous(name, i, System.currentTimeMillis() - startTime, err.getMessage());
1254                         return new CheckResult.Erroneous(name, i, err, Option.none());
1255                     }
1256                 }
1257                 logSatisfied(name, tries, System.currentTimeMillis() - startTime, exhausted);
1258                 return new CheckResult.Satisfied(name, tries, exhausted);
1259             } catch(CheckError err) {
1260                 logErroneous(name, 0, System.currentTimeMillis() - startTime, err.getMessage());
1261                 return new CheckResult.Erroneous(name, 0, err, Option.none());
1262             }
1263         }
1264     }
1265 
1266     /**
1267      * Internally used to model conditions composed of pre- and post-condition.
1268      */
1269     static class Condition {
1270 
1271         static final Condition EX_FALSO_QUODLIBET = new Condition(false, true);
1272 
1273         final boolean precondition;
1274         final boolean postcondition;
1275 
1276         Condition(boolean precondition, boolean postcondition) {
1277             this.precondition = precondition;
1278             this.postcondition = postcondition;
1279         }
1280 
1281         // ¬(p => q) ≡ ¬(¬p ∨ q) ≡ p ∧ ¬q
1282         boolean isFalse() {
1283             return precondition && !postcondition;
1284         }
1285     }
1286 
1287     /**
1288      * Internally used to provide more specific error messages.
1289      */
1290     static class CheckError extends Error {
1291 
1292         private static final long serialVersionUID = 1L;
1293 
1294         CheckError(String message, Throwable cause) {
1295             super(message, cause);
1296         }
1297     }
1298 }